Now that #63 has been merged, we can get to this one. I believe the reorganisation bit is rather uncontroversial, more modularity is always nice. The extra decidability bits, I'd say they don't hurt too much, one can always remove them in a branch or something, as PMP already did for the quoting extension for instance.

The main contentious bit is then maybe the dependency on MetaCoq? I wanted to do a bit of meta-programming, to showcase how "regular" the bidirectional invariants are. However, this adds a nasty dependency, and has a few weird consequences (including the worst: shadowing of tactics). I can work to remove it if this is preferred.

@kyoDralliam @ppedrot what do you say?

I'd prefer to have a dev that is as self-contained as possible, especially when metacoq is such a humongous dep.

Alright, I'll try to make the change. I'll probably simply remove the meta-programming for now (which is the "easy" fix), and maybe later I'll try to port my MetaCoq code to Ltac2, which brings in a less invasive dependency (although note that atm we only depend on template, so the dependency is "reasonable").

Done, MetaCoq removed in 4e63950. I think this is ready for merging. There is still some need for cleanup I think, but these will come as I write the paper I think. I'd say it's best to go forward and get at least this part out of the door.

@kyoDralliam There is quite a large reorganisation, it might wreck your other branch :/ Would you be fine with a somewhat nasty rebasing? Hopefully after that the logical relation and the rest are going to be more tightly separated, so this sort of issues should pop less often.

What's todo.v?

The proof I mentioned the other day that injectivity of term constructors is provable from the existence of the eliminator, that should never have left my computer. Let me get rid of that 😬

Lost in typeclasses shenanigans, now it goes through :)

It's good that someone is mopping up my mess 😬